-
Notifications
You must be signed in to change notification settings - Fork 106
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
refinement proof for AArch64 #668
Conversation
lsf37
commented
Aug 28, 2023
•
edited
Loading
edited
- finish refinement proof between abstract and design spec for AArch64
- finish orphanage proof for AArch64
- proof cleanup for the two above (more to be completed in a separate PR later)
- switch off quick-and-dirty for Refine
- includes ASpec changes (6 bug fixes, 1 invariant strengthening)
- includes design spec changes (2 bug fixes)
befefcb
to
7c3bc2d
Compare
(rebased on master after merge of #656) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a lot of really good work and it's great to see the new corres methods being used and making proofs shorter! All of my suggestions are for pretty minor things.
lemma no_0_page_table: | ||
"\<lbrakk> no_0_obj' s; page_table_at' pt_t 0 s \<rbrakk> \<Longrightarrow> False" |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's only used in one place so it doesn't make much difference, but this would feel more natural to me as
lemma no_0_page_table: | |
"\<lbrakk> no_0_obj' s; page_table_at' pt_t 0 s \<rbrakk> \<Longrightarrow> False" | |
lemma no_0_page_table: | |
"no_0_obj' s \<Longrightarrow> \<not>page_table_at' pt_t 0 s" |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It depends on the use case which of these two makes more sense. The .. ==> False
one is in normal form, so I'd usually prefer that, but if you want to use it for rewriting for instance, the \<not> ..
form is more useful.
In terms of interpretation, the False
form just says there is a contradiction between the two things and is usable symmetrically. The negation form assumes (in this case) a global property and says something local cannot be true because of it. Both make sense, depending on where you want to use them.
I couldn't directly comment on them as part of my review and it's very minor, but a few of the commits had typos in their messages.
|
Quite a few of the lemmas being moved out of Refine and to Lib and AInvs exist in the other architectures as well. Do we want to clean it up for them now as well while it's fresh, or leave it until a future arch split? |
Would make sense to do it soon, but in a separate PR. Better to keep this one on topic for AArch64. |
Thanks for that very detailed review! Will fix those up and rebase before merging. |
This concept no longer makes sense on AARCH64, we will either need to know that certain addresses are in user_region (which implies canonical_user, which is more strict than canonical), or we will need to know they are in the kernel_window, which is also more strict than canonical. We'll only find out for sure in CRefine. Both cases are liftable from valid_vspace_uses and pspace_in_kernel_window from AInvs, so instead of a new invariant, the plan is to use Haskell assertions to transport the relevant info to CRefine when needed. Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Fix two small spec bugs where ASpec was out of sync with Haskell and C. Signed-off-by: Gerwin Klein <[email protected]>
The vmid_table never maps ASID 0. We managed to get through AInvs without this property, but Refine does need it later. Signed-off-by: Gerwin Klein <[email protected]>
Add missing cache machine op. Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
cleanInvalidate should be using cleanInvalidateCacheRange_RAM. Signed-off-by: Gerwin Klein <[email protected]>
Refine needs slightly stricter information about asid maps, in particular we need to know explicitly that asid 0 never maps to a VSpace. This is the reverse of valid_vmid_table, but unfortunately does not fully follow from valid_vmid_table, because there can be VSpaces mapped without an assigned VMID. We shift the test for 0 < asid from entry_for_asid to vspace_for_asid so we can use entry_for_asid in the formulation of the invariant. Signed-off-by: Gerwin Klein <[email protected]>
Main progress is in VSpace_R, with some fallout in ArchAcc_R, ADT_R, and Schedule_R for invariant and spec changes. General obj_at preservation for setVMRoot does not hold and is relegated to something more specific in Schedule_R Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Tweak formulation of createNewCaps for page tables to be in the expected "addr ~elem~ map .." form. The previous definition was not wrong, but the lemmas in Retype_R expect the set membership form. Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Lemma can potentially be removed if not used in the rest of Refine. Signed-off-by: Gerwin Klein <[email protected]>
decode_vspace_invocation operates on vspace flush labels, not page flush labels. Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Rafal Kolanski <[email protected]>
These have either already been resolved, are trivial moves within one theory, or they are questions that the rest of the proof has now answered. Signed-off-by: Gerwin Klein <[email protected]>
Might be useful for later proofs, but no need to fix now. Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
With a slightly better lifting rule, these can all be grouped and proved automatically. Signed-off-by: Gerwin Klein <[email protected]>
With adjustment of ARMMMU_improve_cases, the decode functions can all be done in a single crunch invocation. Signed-off-by: Gerwin Klein <[email protected]>
The (=) syntax is Isabelle, the ML syntax is still (op =) Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Co-authored-by: Rafal Kolanski <[email protected]> Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Collect all operator lifting lemmas in one place under hoare_vcg_op_lift. (Moved from Refine) Move the lifting lemmas that were still in AInvs up to lib. Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
The old version of dom_ucast_eq in AInvs is not useful, because the necessary constants are not available yet in AInvs. Signed-off-by: Gerwin Klein <[email protected]>
7c3bc2d
to
5497666
Compare